(***************************************************************************
* Tactics to Automate Reasoning about Freshness                            *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Set Implicit Arguments.
Require Import List Decidable OrderedType OrderedTypeEx.
Require Import Lib_Tactic Lib_ListFacts Lib_FinSet Lib_FinSetImpl.


(*Ltac fresh_simpl_to_notin_in_context :=
  repeat (match goal with H: fresh _ _ _ |- _ =>
    progress (simpl in H; destructs H) end).
*)

(* ********************************************************************** *)
(** ** Tactics for notin *)

(** For efficiency, we avoid rewrites by splitting equivalence. *)

Module NotInFacts (M : FinSet).
Import M.
Module Export MyFinSetFacts := FinSetFacts M.

Open Local Scope set_scope.

Lemma notin_singleton_r : forall x y,
  x \notin {{y}} -> x <> y.
intros. rewrite* <- notin_singleton.
Qed.

Lemma notin_singleton_l : forall x y,
  x <> y -> x \notin {{y}}.
intros. rewrite* notin_singleton.
Qed.

Lemma notin_singleton_swap : forall x y,
  x \notin {{y}} -> y \notin {{x}}.
intros. apply notin_singleton_l.
apply sym_not_eq. apply* notin_singleton_r.
Qed.

Lemma notin_union_r : forall x E F,
  x \notin (E \u F) -> (x \notin E) /\ (x \notin F).
intros. rewrite* <- notin_union.
Qed.

Lemma notin_union_l : forall x E F,
  x \notin E -> x \notin F -> x \notin (E \u F).
intros. rewrite* notin_union.
Qed.

(** Tactics to deal with notin. It interacts with union
    singleton and empty, but not inclusion. *)

Ltac notin_solve_from x E H :=
  match type of H with x \notin ?L =>
    match L with context[E] =>
      match L with
      | E => exact H
      | ?F \u ?G =>
        let P := constr:(@notin_union_r x F G H) in
        let PF := eval simpl in (proj1 P) in
        let PG := eval simpl in (proj2 P) in
        solve [ notin_solve_from x E PF
              | notin_solve_from x E PG ]
      end
    end
  end.

Ltac notin_solve_from_context x E :=
  match goal with H: x \notin _ |- _ =>
    notin_solve_from x E H end.

Ltac notin_solve_one :=
  match goal with
  | |- _ \notin {} =>
    apply notin_empty
  | |- ?x \notin {{?y}} => (* by x <> y or y <> x *)
    apply notin_singleton_l; solve
    [ assumption | apply sym_not_eq; assumption ]
  | |- ?x \notin {{?y}} => (* by y \notin {{x}} *)
    apply notin_singleton_swap; notin_solve_from_context y ({{x}})
  | |- ?x \notin ?E  =>    (* default search *)
    notin_solve_from_context x E
  end.

Ltac notin_simpl :=
  try match goal with |- _ \notin (_ \u _) =>
    apply notin_union_l; notin_simpl end.

Ltac notin_simpl_hyps := (* forward-chaining *)
  try match goal with
  | H: _ \notin {} |- _ =>
     clear H; notin_simpl_hyps
  | H: ?x \notin {{?y}} |- _ =>
     puts (@notin_singleton_r x y H);
     clear H; notin_simpl_hyps
   | H: ?x \notin (?E \u ?F) |- _ =>
     let H1 := fresh "Fr" in let H2 := fresh "Fr" in
     destruct (@notin_union_r x E F H) as [H1 H2];
     clear H; notin_simpl_hyps
  end.

Ltac notin_simpls :=
  notin_simpl_hyps; notin_simpl.

Ltac notin_solve :=
  notin_simpl; notin_solve_one.

Ltac notin_contradiction :=
  match goal with H: ?x \notin ?E |- _ =>
    match E with context[x] =>
      let K := fresh in assert (K : x \notin {{x}});
        [ notin_solve_one
        | contradictions; apply (notin_same K) ]
    end
  end.

Ltac notin_neq_solve :=
  apply notin_singleton_r; notin_solve.


(* ********************************************************************** *)
(** Demo for notin *)

Lemma test_notin_solve_1 : forall x E F G,
  x \notin E \u F -> x \notin G -> x \notin (E \u G).
intros. notin_solve.
Qed.

Lemma test_notin_solve_2 : forall x y E F G,
  x \notin E \u {{y}} \u F -> x \notin G ->
  x \notin {{y}} /\ y \notin {{x}}.
intros. split. notin_solve. notin_solve.
Qed.

Lemma test_notin_solve_3 : forall x y,
  x <> y -> x \notin {{y}} /\ y \notin {{x}}.
intros. split. notin_solve. notin_solve.
Qed.

Lemma test_notin_contradiction : forall x y E F G,
  x \notin (E \u {{x}} \u F) -> y \notin G.
intros. notin_contradiction.
Qed.

Lemma test_neq_solve : forall x y E F,
  x \notin (E \u {{y}} \u F) -> y \notin E ->
  y <> x /\ x <> y.
intros. split. notin_neq_solve. notin_neq_solve.
Qed.



(***************************************************************************)
(** Automation: hints to solve "notin" subgoals automatically. *)

Hint Extern 1 (_ \notin _) => notin_solve.

Hint Extern 1 (_ \in _ -> False) =>
  repeat match goal with
  | H: context [?x \in ?E -> False] |- _ => 
    fold (not (x \in E)) in H 
  | |- context [?x \in ?E -> False] => 
    fold (not (x \in E)) end.

(*Hint Extern 1 (_ <> _ :> var) => notin_neq_solve.*)
Hint Extern 1 (_ <> _ :> S.elt) => notin_neq_solve.
End NotInFacts.